Nuprl Lemma : select_tl
2,24
postcript
pdf
A
:Type,
as
:
A
List,
n
:
(||
as
||-1). tl(
as
)[
n
] =
as
[
n
+1]
A
latex
Definitions
True
,
T
,
Prop
,
l
[
i
]
,
P
Q
,
P
Q
,
P
Q
,
False
,
A
,
P
&
Q
,
A
B
,
i
j
<
k
,
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
{
i
..
j
}
,
tl(
l
)
Lemmas
int
seg
wf
,
length
wf1
,
select
cons
tl
,
select
wf
,
squash
wf
,
le
wf
origin
A:Type, as:A List, n:
(||as||-1). tl(as)[n] = as[n+1] 
A A:Type, as:A List, n:(||as||-1). tl(as)[n] = as[n+1] A 
T
Q
Q Q
A
B j < k Tx:A. B(x)
}